Inference at * 2 1 1 1 1 1 
Iof proof for Lemma member nth tl:

.....falsecase..... NILNIL

1. T : Type
2. n : 
3. 0 < n
4. x:T, L:(T List). (x  nth_tl(n - 1;L))  (x  L)
5. T
6. T List
7. n1 : 
8. 0 < n1
9. nth_tl(n1 - 1;[]) = []
10. 0 < n1
  nth_tl(n1 - 1;tl([])) = [] 

latex

 by ((Reduce 0) 
CollapseTHEN (Auto)) 

latex

C.

Definitions

tl(l)